0-In Announces Breakthrough Deep Counterexample Technology to Find the Toughest RTL Bugs Before Silicon
SAN JOSE, Calif. - January 27, 2003 - Today 0-In Design Automation, the Assertion-Based Verification Company, announced a new formal verification technology called "deep counterexample" (DCE) technology. DCE technology eliminates essentially all tough bugs of three critical bug types in complex ASICs and System-on-Chip (SoC) devices. The new technology is available in 0-In Confirm, a new product that is included in V2.0 of 0-In's Assertion-Based Verification (ABV) Suite. (See today's release entitled "0-In Announces New Products Based on Breakthrough Formal Verification Algorithms" for product details).
Despite using more than half of total project resources for functional verification, most SoC devices have corner-case bugs in first silicon. Detecting, diagnosing and fixing such bugs is a difficult and time-consuming process that can cost millions of dollars and frequently causes chips to miss their market windows. 0-In's breakthrough DCE technology helps design and verification teams reach functional verification closure by finding tough RTL design bugs that are missed by every other verification method.
Verifying bug fixes with formal methods is faster and more predictable than with simulation alone. 0-In's DCE technology exhaustively verifies assertions to a much greater depth than any other commercially available formal verification product. In addition to finding tough bugs before tape-out, DCE technology can be used to verify that late-stage bug fixes are correct.
Eliminating common bug types
To achieve first-silicon success, designers must detect and eliminate various types of bugs. 0-In provides a full suite of ABV tools that address the following five bug types:
- Control-logic corner-case bugs
- Data loss across clock domains
- Interface bugs (non-compliance and omission)
- Low-probability, data-dependent bugs
- Simulation-to-synthesis mismatches
0-In's ABV Suite combines effective assertion specification, easy assertion maintenance, efficient assertion checker simulation, leading-edge static and dynamic formal algorithms, and unique DCE technology to find essentially all of these bugs in complex chip designs.
0-In's DCE technology, focuses on three of these bug types: control-logic corner-case bugs, interface bugs (non-compliance and omission), and low-probability, data-dependent bugs. (See today's related releases for information on how 0-In handles data loss across clock domains and simulation-to-synthesis mismatches.)
Control-logic corner-case bugs
Many bugs that end up in silicon are due to a combination of control-logic corner cases that are not exercised during simulation. For example, a processor might fail when a particular instruction is in a specific pipeline stage at the same time that a data FIFO is full and a cache miss occurs and a specific interrupt arrives. Only formal verification, with its ability to exhaustively explore all possible interactions of corner-case behaviors, can reliably detect this type of bug before first silicon. 0-In Confirm is the first product that is able to find essentially all such bugs pre-silicon.
Interface bugs (non-compliance and omission)
Bugs associated with complex interfaces can be very difficult to find, especially because the interface rules may not be fully understood by the design team. 0-In's ABV suite provides an effective solution for interface verification. 0-In's CheckerWare library provides a rich selection of protocol monitors, each of which captures all the rules of a single standard interface protocol in a format that is compatible with both simulation and formal verification. 0-In Check adds these monitors to simulation, allowing detection of any protocol violations. After simulation, 0-In Search and 0-In Confirm bring the power of formal verification to bear on the interface design using the same protocol monitors.
0-In Confirm uses DCE technology to find tough interface bugs that simulation misses, including bugs of non-compliance (i.e., protocol behavior implemented incorrectly) and bugs of omission (i.e., protocol behavior not implemented at all). Bugs of omission are particularly difficult to find using simulation because the test writer may be completely unaware of the omitted behavior and may fail to create any tests for it.
Low-probability, data-value bugs
Low-probability, data-value bugs require a specific data value to occur on a wide input variable during a specific cycle. These bugs require highly improbable stimuli and are unlikely to be detected in simulation using hand-written or pseudo-random tests. 0-In Confirm uses DCE technology to home in on exactly the right value in exactly the right cycle, exposing essentially all low-probability, data-value bugs.
About 0-In
0-In Design Automation, Inc. (pronounced "zero-in") develops and supports functional verification products that help verify multi-million gate application-specific integrated circuit (ASIC) and system-on-chip (SoC) designs. The company delivers a comprehensive assertion-based verification (ABV) solution that provides value throughout the design and verification cycle - from the block level to the chip and system level. Twelve of the 15 largest electronics companies have adopted 0-In tools and methodologies in their integrated circuit (IC) design verification flows. 0-In was founded in 1996 and is based in San Jose, Calif. For more information, see http://www.0-in.com.
